COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	This is a request for a grant of xxx to the Computer Science Department
C00009 ENDMK
C⊗;
This is a request for a grant of xxx to the Computer Science Department
of Stanford University for the purpose of developing an interactive
proof-checker oriented to the verification of LISP programs by
students learning to compute with symbolic expressions.

A computer program is a mathematical object, and it has always seemed
disgraceful that programs are debugged, i.e. tried out on cases until
the programmer is satisfied or at least tired.  A program should be
proved to meet its specifications.
Since it is an explicit part of the notion of formal proof that it can
be mechanically checked, one can imagine providing formal proofs that
computer programs meet their specifications and checking these proofs
by computer program.  This would provide much greater assurance that
a program is correct than mere debugging.

Mathematical formalisms have
existed since the 1930s within which proofs exist that algorithms
meet their specifications, but fully formal proofs
of program correctness have never been written in these formalisms,
because they are orders of magnitude longer than the customary
informal proofs.  Instead students of the formal systems have
contented themselves with informal proofs that the desired formal
proofs exist.

Since the early 1960s it has been a major objective of the branch
of computer science called mathematical theory of computation to
provide formal systems within which proofs of program correctness
are easy to develop and no longer than the informal proofs.  This
goal has not been fully achieved for all classes of programs, but
enough progress has been made so that techniques of program proving
have been successfully introduced into programming courses as well
as in specialized courses in mathematical theory of computation.

New developments reported in [Cartwright 1977] and [McCarthy 1978]
have made this practical for pure LISP - a programming language
of considerable practical use and which is taught in many universities.
Since Spring 1977, increasing amounts of program proving have
been introduced into the elementary LISP programming course taught
at Stanford University.  It has been possible to include in final
examinations problems that require a student to write a program
that performs a certain task and prove that the program does it.
These proofs have been informal and not machine checked.

Besides that, since 1972 the Stanford University Artificial
Intelligence Laboratory has had a proof checking program for
first order logic called FOL.  The Cartwright-McCarthy technique
which involves expressing LISP programs as sentences of first order logic
has been well suited to program proving in FOL, and a
number of substantial programs have been proved.

Unfortunately, FOL is unsuited for use in an elementary programming
course, although it has been used successfully in specialized
courses in mathematical theory of computation.  The problem comes from
the facts that
programming courses have large number of students, and it is not
reasonable to devote more than one third of the time to program
proving in order to devote enough time to describing the language
and techniques of programming.

FOL has many grammatical crochets, so that mistakes in using it
are frequent.  It runs slowly so that we can't afford the computer
time to let large numbers of students fumble with it.  Moreover, it
is not at all integrated with the MACLISP system in which the students
write their programs.

The object of this proposal is to develop an interactive proof-checker
integrated with the MACLISP system in which the students program
that will enable a student to prove many of his programs correct
immediately after writing them.  We hope to put in enough simplifications
into the proof-checker so that in many cases the student has only
to describe the mathematical induction step and the machine does the
rest.  Techniues for this have been developed by Richard Weyhrauch [1978]
and also by Robert Boyer and J. Moore [1978].